| Definitions | t  T, P   Q,  x:A. B(x), FairFifo, x:A  B(x), E, IdLnk, {i..j },  b, s = t,  , x:A B(x), P & Q, A & B,  x:A. B(x), World, i j, {x:A| B(x) }, sends(l;e), Msg,  , a<b, Void, False,  A, A B, i j < k, #$n, time(e), n+m, snds(l;t), ||as||, upto(n),  x:A. B(x), Top, {T}, SQType(T), Prop, s ~ t,  b,  , i=j, P  Q, Unit, left+right, n-m, type List, S  T, m(l;t), nil, car.cdr,  x.A(x), Type, map(f;as), <a,b>, True, P Q,  T, loc(e), m(i;t), onlnk(l;mss), source(l), Id, P  Q, Dec(P), a = b, rcvs(l;t), destination(l), a(i;t), isrcv(l;a), Action(i), filter(P;l), f(a), S  T, x. t(x), 2of(t), 1of(t), isnull(a), index(e), sender(e), lnk(k), a = b, p  q, act(e), kind(e), kind(a), isrcv(k), p = q, match(l;t;t'), mu(f), t ...$L |
| Lemmas | length nil, decidable equal Id, assert of band, and functionality wrt iff, w-match-unique, mu-property, mu wf, w-match wf, member wf, assert-w-match, cand functionality wrt iff, assert-w-eq-E-iff, w-eq-E wf, assert-eq-lnk, w-index wf, w-ekind wf, w-sender wf, band wf, isrcv wf, eq lnk wf, lnk wf, w-kind wf, w-rcvs wf, pi1 wf, pi2 wf, w-isnull wf, false wf, filter wf, filter map upto2, w-a wf, w-isrcvl wf, w-action wf, ldst wf, decidable assert, assert-eq-id, eq id wf, Id wf, squash wf, true wf, length append, lsrc wf, w-onlnk-m, w-loc wf, concat append, concat-cons, append nil sq, map wf, le wf, w-ml wf, top wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, map append sq, upto wf, int seg wf, IdLnk wf, w-E wf, length wf1, w-snds wf, non neg length, nat wf, w-time wf, w-Msg wf, w-sends wf, world wf, fair-fifo wf, w-snd-rcv |
